loc:Id, ds:x:Id fp Type, knd:Knd, T:Type, x:Id, f:(State(ds)TDeclaredType(ds;x)).
R-Feasible(@loc effect knd(v:T)  x := f State(ds) v )  x  dom(ds) 

latex

Definitions	x:A. B(x), P  Q, R-Feasible(R), P & Q, t  T, Prop, x. t(x), f(x)?z, if b t else f fi, true, false, Top, State(ds), x:A. B(x), True, x(s), , Unit, P  Q,
Lemmas	normal-ds wf, normal-type wf, assert wf, isrcv wf, Id wf, ldst wf, lnk wf, decl-state wf, decl-type wf, Knd wf, fpf wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, bool wf, eqtt to assert, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, true wf